es:ES, ff:FIFO, f2f+:F2F+-decls.
(ff.C r Id) & (i, j:ff.C. @i(awaiting (i,j):)) & (i, j:ff.C. @i(owes_ack (i,j):))
& (i:ff.C, e:E. (ff.R(i,e))  (loc(e) = i  Id))
& (e:E. Dec(is_req  (e)))
& (e:E. Dec(is_ack (e)))
& (i:ff.C, e:E. Dec(ff.R(i,e)))
& (i, j:ff.C, e:E. Dec(ff.S(i,j,e)))
& (i, j:ff.C, e:E. (ff.S(i,j,e))  (loc(e) = i  Id))
& (e:E, sndr, rcvr:ff.C. ([e: sndr is_req   rcvr] & [e: rcvr is_ack  sndr])) 

latex

Definitions	t  T, A c B, t.2, t.1, , is_ack , is_req  , P  Q, owes_ack , awaiting , P & Q, F2F+-decls, FIFO, x:A. B(x)
Lemmas	event system wf, fifo wf, es-state wf, top wf, snd-it wf, not wf, fifoS wf, decidable wf, es-loc wf, fifoR wf, bool wf, es-dtype wf, Id wf, es-E wf, fifoC wf